Skip to content

feat(abi-emit-manifest): emit ABI manifest from Idris2 source (standa…#30

Closed
hyperpolymath wants to merge 1 commit into
mainfrom
feat/abi-verify-phase1b-emitter
Closed

feat(abi-emit-manifest): emit ABI manifest from Idris2 source (standa…#30
hyperpolymath wants to merge 1 commit into
mainfrom
feat/abi-verify-phase1b-emitter

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

…rds#92 Phase 1b)

Phase 1b of standards#89 sub-issue 3 / standards#92. Adds the abi-emit-manifest subcommand, which parses a cartridge's Safe*.idr and emits the JSON manifest the existing abi-verify subcommand consumes. Together with Phase 1 this closes the loop: the Idris2 source is now the single authority — the manifest is derived, not hand-authored.

Scope

Parses the cartridge convention shape:

  • data <Enum> = A | B | C (one-line or multi-line; with or without parameterised variants like Custom String)
  • <fn> : <Enum> -> Int type signatures (associates each enum with its *ToInt function; necessary because the convention is loose — SsgEngine uses engineToInt, K9Format uses formatToInt, not the naive ssgEngineToInt etc.)
  • <fn> <variant> = <int> value-encoding equations (including parameterised forms like (Custom _) = 99)
  • canTransition <From> <To> = True allowed-transition equations (catch-all _ _ = False skipped; the verifier already catches accept-by-omission as drift)

Not a general Idris2 parser; deliberately shape-specific.

End-to-end smoke

$ iseriser abi-emit-manifest \
    --idris ../boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr \
    --cartridge ssg-mcp \
    --source-path "boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr" \
    --out /tmp/ssg.json
abi-emit-manifest: wrote /tmp/ssg.json (2 enums, 11 transitions)

$ iseriser abi-verify --manifest /tmp/ssg.json \
    --zig-ffi ../boj-server/cartridges/ssg-mcp/ffi/ssg_ffi.zig
abi-verify: OK — cartridge `ssg-mcp` ABI manifest agrees with `…/ssg_ffi.zig`

Same for k9iser-mcp (2 enums, 10 transitions, verify clean).

The diff between hand-authored and emitted manifests is just JSON formatting + the absence of the allowed:false safety-invariant rows (documented in README.adoc — the verifier's
transition-accepted-but-undeclared finding covers the same drift class, so safety is preserved). Verify result is identical.

Tests

6 new unit tests in idris_emitter::tests:

  • one-line data declaration
  • multi-line data declaration with parameterised variant
  • type-signature-based fn↔enum association (the SsgEngine→engineToInt case)
  • variant without ToInt mapping is dropped
  • canTransition parsing skips the catch-all
  • Idris2 doc-comment stripping

39 lib tests green (was 33).

Next: Phase 2 — wire the emit→verify pair into per-cartridge CI.

Refs hyperpolymath/standards#92
Refs hyperpolymath/standards#89

Summary

Changes

RSR Quality Checklist

Required

  • Tests pass (just test or equivalent)
  • Code is formatted (just fmt or equivalent)
  • Linter is clean (no new warnings or errors)
  • No banned language patterns (no TypeScript, no npm/bun, no Go/Python)
  • No unsafe blocks without // SAFETY: comments
  • No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry)
  • SPDX license headers present on all new/modified source files
  • No secrets, credentials, or .env files included

As Applicable

  • .machine_readable/STATE.a2ml updated (if project state changed)
  • .machine_readable/ECOSYSTEM.a2ml updated (if integrations changed)
  • .machine_readable/META.a2ml updated (if architectural decisions changed)
  • Documentation updated for user-facing changes
  • TOPOLOGY.md updated (if architecture changed)
  • CHANGELOG or release notes updated
  • New dependencies reviewed for license compatibility (PMPL-1.0-or-later / MPL-2.0)
  • ABI/FFI changes validated (src/interface/abi/ and src/interface/ffi/ consistent)

Testing

Screenshots

…rds#92 Phase 1b)

Phase 1b of standards#89 sub-issue 3 / standards#92. Adds the
`abi-emit-manifest` subcommand, which parses a cartridge's `Safe*.idr`
and emits the JSON manifest the existing `abi-verify` subcommand
consumes. Together with Phase 1 this closes the loop: the Idris2 source
is now the **single authority** — the manifest is derived, not
hand-authored.

## Scope

Parses the cartridge convention shape:

  * `data <Enum> = A | B | C` (one-line or multi-line; with or without
    parameterised variants like `Custom String`)
  * `<fn> : <Enum> -> Int` type signatures (associates each enum with
    its `*ToInt` function; necessary because the convention is loose —
    `SsgEngine` uses `engineToInt`, `K9Format` uses `formatToInt`,
    not the naive `ssgEngineToInt` etc.)
  * `<fn> <variant> = <int>` value-encoding equations (including
    parameterised forms like `(Custom _) = 99`)
  * `canTransition <From> <To> = True` allowed-transition equations
    (catch-all `_ _ = False` skipped; the verifier already catches
    accept-by-omission as drift)

Not a general Idris2 parser; deliberately shape-specific.

## End-to-end smoke

```
$ iseriser abi-emit-manifest \
    --idris ../boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr \
    --cartridge ssg-mcp \
    --source-path "boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr" \
    --out /tmp/ssg.json
abi-emit-manifest: wrote /tmp/ssg.json (2 enums, 11 transitions)

$ iseriser abi-verify --manifest /tmp/ssg.json \
    --zig-ffi ../boj-server/cartridges/ssg-mcp/ffi/ssg_ffi.zig
abi-verify: OK — cartridge `ssg-mcp` ABI manifest agrees with `…/ssg_ffi.zig`
```

Same for `k9iser-mcp` (2 enums, 10 transitions, verify clean).

The diff between hand-authored and emitted manifests is just JSON
formatting + the absence of the `allowed:false` safety-invariant rows
(documented in README.adoc — the verifier's
`transition-accepted-but-undeclared` finding covers the same drift
class, so safety is preserved). Verify result is identical.

## Tests

6 new unit tests in `idris_emitter::tests`:
  * one-line data declaration
  * multi-line data declaration with parameterised variant
  * type-signature-based fn↔enum association (the SsgEngine→engineToInt case)
  * variant without ToInt mapping is dropped
  * canTransition parsing skips the catch-all
  * Idris2 doc-comment stripping

39 lib tests green (was 33).

Next: Phase 2 — wire the emit→verify pair into per-cartridge CI.

Refs hyperpolymath/standards#92
Refs hyperpolymath/standards#89

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath
Copy link
Copy Markdown
Owner Author

Closing as superseded. Branch tip (feat(abi-emit-manifest): emit ABI manifest from Idris2 source (standards#92 Phase 1b)) was already merged via #14. Re-diff vs current main shows merging this branch would delete ~1979 lines of subsequently-merged work (idris_emitter.rs, manifest_schema.rs, cartridge.rs, etc.) — net regression.

@hyperpolymath hyperpolymath deleted the feat/abi-verify-phase1b-emitter branch May 21, 2026 07:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant